the_w:World, l:IdLnk, i:Id, a:Action(i).
isrcv(l;a)  {isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l} 

latex

Definitions	isnull(a), isrcv(k), kind(a), Action(i), Id, World, isrcv(l;a), p  q, Unit, , Prop, b, a = b, {T}, b, A, False, True, IdLnk, P  Q, P & Q, t  T, lnk(k), x:A. B(x), P  Q
Lemmas	lnk wf, assert-eq-lnk, false wf, w-kind wf, eq lnk wf, assert wf, isrcv wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, w-isnull wf, world wf, IdLnk wf, Id wf, w-action wf, w-isrcvl wf